ES
== E:Type
== EqDecider(E)
== pred?:(E(E+Unit))
== info:(E(IdId+(IdLnkE)Id))
== EOrderAxioms(E; pred?; info)
== T:(IdIdType)
== V:(IdIdType)
== M:(IdLnkIdType)
== init:(i,x:IdT(i,x))
== Trans:(i:Idk:Kndkindcase(k; a.V(i,a); l,t.M(l,t) )(x:IdT(i,x))(x:IdT(i,x)))
== val:(e:Ekindcase(kind(e); a.V(loc(e),a); l,t.M(l,t) ))
== Send:(i:Idk:Kndkindcase(k; a.V(i,a); l,t.M(l,t) )(x:IdT(i,x))(Msg(M) List))
== Choose:(i,a:Id(x:IdT(i,x))(V(i,a)+Unit))
== val-axiom(E;V;M;info;pred?;
== val-axiom(init;Trans;Choose;
== val-axiom(Send;val)
== ((i, x:Id. AtomFree(Type;T(i,x)))
== (& (i, a:Id. AtomFree(Type;V(i,a)))
== (& (l:IdLnk, tg:Id. AtomFree(Type;M(l,tg))))
== Top 

latex

---

clarification:

ES{i}
== E:Type{i}
== EqDecider(E)
== pred?:(E(E+Unit))
== info:(E(IdId+(IdLnkE)Id))
== EOrderAxioms{i}(E;
== EOpred?;
== EOinfo)
== T:(IdIdType{i})
== V:(IdIdType{i})
== M:(IdLnkIdType{i})
== init:(i:Idx:IdT(i,x))
== Trans:(i:Idk:Kndkindcase(k; a.V(i,a); l,t.M(l,t) )(x:IdT(i,x))(x:IdT(i,x)))
== val:(e:Ekindcase(kind(info;e); a.V(loc(info;e),a); l,t.M(l,t) ))
== Send:(i:Idk:Kndkindcase(k; a.V(i,a); l,t.M(l,t) )(x:IdT(i,x))(Msg(M) List))
== Choose:(i:Ida:Id(x:IdT(i,x))(V(i,a)+Unit))
== val-axiom(E;V;M;info;pred?;
== val-axiom(init;Trans;Choose;
== val-axiom(Send;val)
== ((i:Id, x:Id. AtomFree(Type{i};T(i,x)))
== (& (i:Id, a:Id. AtomFree(Type{i};V(i,a)))
== (& (l:IdLnk, tg:Id. AtomFree(Type{i};M(l,tg))))
== Top 

latex

Definitions	EqDecider(T), EOrderAxioms(E; pred?; info), kind(e), loc(e), Knd, kindcase(k; a.f(a); l,t.g(l;t) ), type List, Msg(M), x:AB(x), left+right, Unit, val-axiom(E;V;M;info;pred?;init;Trans;Choose;Send;val), x:AB(x), P & Q, IdLnk, x:A. B(x), Id, AtomFree(T;x), Type, f(a), Top
FDL editor aliases	ES